Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
process2(store, m) -> if13(store, m, leq2(m, length1(store)))
if13(store, m, true) -> if23(store, m, empty1(fstsplit2(m, store)))
if13(store, m, false) -> if33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
if23(store, m, false) -> process2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
if33(store, m, false) -> process2(sndsplit2(m, app2(map_f2(self, nil), store)), m)

Q is empty.


↳ QTRS
  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
process2(store, m) -> if13(store, m, leq2(m, length1(store)))
if13(store, m, true) -> if23(store, m, empty1(fstsplit2(m, store)))
if13(store, m, false) -> if33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
if23(store, m, false) -> process2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
if33(store, m, false) -> process2(sndsplit2(m, app2(map_f2(self, nil), store)), m)

Q is empty.

Using Dependency Pairs [1,13] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

IF33(store, m, false) -> SNDSPLIT2(m, app2(map_f2(self, nil), store))
PROCESS2(store, m) -> LENGTH1(store)
SNDSPLIT2(s1(n), cons2(h, t)) -> SNDSPLIT2(n, t)
IF23(store, m, false) -> PROCESS2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
IF33(store, m, false) -> PROCESS2(sndsplit2(m, app2(map_f2(self, nil), store)), m)
IF23(store, m, false) -> APP2(map_f2(self, nil), sndsplit2(m, store))
IF13(store, m, true) -> FSTSPLIT2(m, store)
IF23(store, m, false) -> MAP_F2(self, nil)
MAP_F2(pid, cons2(h, t)) -> APP2(f2(pid, h), map_f2(pid, t))
IF13(store, m, true) -> EMPTY1(fstsplit2(m, store))
PROCESS2(store, m) -> IF13(store, m, leq2(m, length1(store)))
IF33(store, m, false) -> APP2(map_f2(self, nil), store)
FSTSPLIT2(s1(n), cons2(h, t)) -> FSTSPLIT2(n, t)
IF13(store, m, true) -> IF23(store, m, empty1(fstsplit2(m, store)))
IF13(store, m, false) -> MAP_F2(self, nil)
IF13(store, m, false) -> FSTSPLIT2(m, app2(map_f2(self, nil), store))
IF13(store, m, false) -> EMPTY1(fstsplit2(m, app2(map_f2(self, nil), store)))
APP2(cons2(h, t), x) -> APP2(t, x)
IF33(store, m, false) -> MAP_F2(self, nil)
LENGTH1(cons2(h, t)) -> LENGTH1(t)
IF23(store, m, false) -> SNDSPLIT2(m, store)
PROCESS2(store, m) -> LEQ2(m, length1(store))
IF13(store, m, false) -> IF33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
LEQ2(s1(n), s1(m)) -> LEQ2(n, m)
MAP_F2(pid, cons2(h, t)) -> MAP_F2(pid, t)
IF13(store, m, false) -> APP2(map_f2(self, nil), store)

The TRS R consists of the following rules:

fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
process2(store, m) -> if13(store, m, leq2(m, length1(store)))
if13(store, m, true) -> if23(store, m, empty1(fstsplit2(m, store)))
if13(store, m, false) -> if33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
if23(store, m, false) -> process2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
if33(store, m, false) -> process2(sndsplit2(m, app2(map_f2(self, nil), store)), m)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

IF33(store, m, false) -> SNDSPLIT2(m, app2(map_f2(self, nil), store))
PROCESS2(store, m) -> LENGTH1(store)
SNDSPLIT2(s1(n), cons2(h, t)) -> SNDSPLIT2(n, t)
IF23(store, m, false) -> PROCESS2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
IF33(store, m, false) -> PROCESS2(sndsplit2(m, app2(map_f2(self, nil), store)), m)
IF23(store, m, false) -> APP2(map_f2(self, nil), sndsplit2(m, store))
IF13(store, m, true) -> FSTSPLIT2(m, store)
IF23(store, m, false) -> MAP_F2(self, nil)
MAP_F2(pid, cons2(h, t)) -> APP2(f2(pid, h), map_f2(pid, t))
IF13(store, m, true) -> EMPTY1(fstsplit2(m, store))
PROCESS2(store, m) -> IF13(store, m, leq2(m, length1(store)))
IF33(store, m, false) -> APP2(map_f2(self, nil), store)
FSTSPLIT2(s1(n), cons2(h, t)) -> FSTSPLIT2(n, t)
IF13(store, m, true) -> IF23(store, m, empty1(fstsplit2(m, store)))
IF13(store, m, false) -> MAP_F2(self, nil)
IF13(store, m, false) -> FSTSPLIT2(m, app2(map_f2(self, nil), store))
IF13(store, m, false) -> EMPTY1(fstsplit2(m, app2(map_f2(self, nil), store)))
APP2(cons2(h, t), x) -> APP2(t, x)
IF33(store, m, false) -> MAP_F2(self, nil)
LENGTH1(cons2(h, t)) -> LENGTH1(t)
IF23(store, m, false) -> SNDSPLIT2(m, store)
PROCESS2(store, m) -> LEQ2(m, length1(store))
IF13(store, m, false) -> IF33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
LEQ2(s1(n), s1(m)) -> LEQ2(n, m)
MAP_F2(pid, cons2(h, t)) -> MAP_F2(pid, t)
IF13(store, m, false) -> APP2(map_f2(self, nil), store)

The TRS R consists of the following rules:

fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
process2(store, m) -> if13(store, m, leq2(m, length1(store)))
if13(store, m, true) -> if23(store, m, empty1(fstsplit2(m, store)))
if13(store, m, false) -> if33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
if23(store, m, false) -> process2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
if33(store, m, false) -> process2(sndsplit2(m, app2(map_f2(self, nil), store)), m)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 7 SCCs with 15 less nodes.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
            ↳ QDPOrderProof
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APP2(cons2(h, t), x) -> APP2(t, x)

The TRS R consists of the following rules:

fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
process2(store, m) -> if13(store, m, leq2(m, length1(store)))
if13(store, m, true) -> if23(store, m, empty1(fstsplit2(m, store)))
if13(store, m, false) -> if33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
if23(store, m, false) -> process2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
if33(store, m, false) -> process2(sndsplit2(m, app2(map_f2(self, nil), store)), m)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].


The following pairs can be oriented strictly and are deleted.


APP2(cons2(h, t), x) -> APP2(t, x)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial Order [17,21] with Interpretation:

POL( cons2(x1, x2) ) = x1 + x2 + 1


POL( APP2(x1, x2) ) = x1 + x2



The following usable rules [14] were oriented: none



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
            ↳ QDPOrderProof
              ↳ QDP
                ↳ PisEmptyProof
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
process2(store, m) -> if13(store, m, leq2(m, length1(store)))
if13(store, m, true) -> if23(store, m, empty1(fstsplit2(m, store)))
if13(store, m, false) -> if33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
if23(store, m, false) -> process2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
if33(store, m, false) -> process2(sndsplit2(m, app2(map_f2(self, nil), store)), m)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

MAP_F2(pid, cons2(h, t)) -> MAP_F2(pid, t)

The TRS R consists of the following rules:

fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
process2(store, m) -> if13(store, m, leq2(m, length1(store)))
if13(store, m, true) -> if23(store, m, empty1(fstsplit2(m, store)))
if13(store, m, false) -> if33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
if23(store, m, false) -> process2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
if33(store, m, false) -> process2(sndsplit2(m, app2(map_f2(self, nil), store)), m)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].


The following pairs can be oriented strictly and are deleted.


MAP_F2(pid, cons2(h, t)) -> MAP_F2(pid, t)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial Order [17,21] with Interpretation:

POL( cons2(x1, x2) ) = x2 + 1


POL( MAP_F2(x1, x2) ) = x2



The following usable rules [14] were oriented: none



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
              ↳ QDP
                ↳ PisEmptyProof
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
process2(store, m) -> if13(store, m, leq2(m, length1(store)))
if13(store, m, true) -> if23(store, m, empty1(fstsplit2(m, store)))
if13(store, m, false) -> if33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
if23(store, m, false) -> process2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
if33(store, m, false) -> process2(sndsplit2(m, app2(map_f2(self, nil), store)), m)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

LENGTH1(cons2(h, t)) -> LENGTH1(t)

The TRS R consists of the following rules:

fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
process2(store, m) -> if13(store, m, leq2(m, length1(store)))
if13(store, m, true) -> if23(store, m, empty1(fstsplit2(m, store)))
if13(store, m, false) -> if33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
if23(store, m, false) -> process2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
if33(store, m, false) -> process2(sndsplit2(m, app2(map_f2(self, nil), store)), m)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].


The following pairs can be oriented strictly and are deleted.


LENGTH1(cons2(h, t)) -> LENGTH1(t)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial Order [17,21] with Interpretation:

POL( cons2(x1, x2) ) = x2 + 1


POL( LENGTH1(x1) ) = x1



The following usable rules [14] were oriented: none



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
              ↳ QDP
                ↳ PisEmptyProof
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
process2(store, m) -> if13(store, m, leq2(m, length1(store)))
if13(store, m, true) -> if23(store, m, empty1(fstsplit2(m, store)))
if13(store, m, false) -> if33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
if23(store, m, false) -> process2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
if33(store, m, false) -> process2(sndsplit2(m, app2(map_f2(self, nil), store)), m)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
          ↳ QDP
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

LEQ2(s1(n), s1(m)) -> LEQ2(n, m)

The TRS R consists of the following rules:

fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
process2(store, m) -> if13(store, m, leq2(m, length1(store)))
if13(store, m, true) -> if23(store, m, empty1(fstsplit2(m, store)))
if13(store, m, false) -> if33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
if23(store, m, false) -> process2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
if33(store, m, false) -> process2(sndsplit2(m, app2(map_f2(self, nil), store)), m)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].


The following pairs can be oriented strictly and are deleted.


LEQ2(s1(n), s1(m)) -> LEQ2(n, m)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial Order [17,21] with Interpretation:

POL( s1(x1) ) = x1 + 1


POL( LEQ2(x1, x2) ) = x1



The following usable rules [14] were oriented: none



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
              ↳ QDP
                ↳ PisEmptyProof
          ↳ QDP
          ↳ QDP
          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
process2(store, m) -> if13(store, m, leq2(m, length1(store)))
if13(store, m, true) -> if23(store, m, empty1(fstsplit2(m, store)))
if13(store, m, false) -> if33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
if23(store, m, false) -> process2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
if33(store, m, false) -> process2(sndsplit2(m, app2(map_f2(self, nil), store)), m)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

SNDSPLIT2(s1(n), cons2(h, t)) -> SNDSPLIT2(n, t)

The TRS R consists of the following rules:

fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
process2(store, m) -> if13(store, m, leq2(m, length1(store)))
if13(store, m, true) -> if23(store, m, empty1(fstsplit2(m, store)))
if13(store, m, false) -> if33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
if23(store, m, false) -> process2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
if33(store, m, false) -> process2(sndsplit2(m, app2(map_f2(self, nil), store)), m)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].


The following pairs can be oriented strictly and are deleted.


SNDSPLIT2(s1(n), cons2(h, t)) -> SNDSPLIT2(n, t)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial Order [17,21] with Interpretation:

POL( SNDSPLIT2(x1, x2) ) = x1


POL( cons2(x1, x2) ) = max{0, -1}


POL( s1(x1) ) = x1 + 1



The following usable rules [14] were oriented: none



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
              ↳ QDP
                ↳ PisEmptyProof
          ↳ QDP
          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
process2(store, m) -> if13(store, m, leq2(m, length1(store)))
if13(store, m, true) -> if23(store, m, empty1(fstsplit2(m, store)))
if13(store, m, false) -> if33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
if23(store, m, false) -> process2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
if33(store, m, false) -> process2(sndsplit2(m, app2(map_f2(self, nil), store)), m)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

FSTSPLIT2(s1(n), cons2(h, t)) -> FSTSPLIT2(n, t)

The TRS R consists of the following rules:

fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
process2(store, m) -> if13(store, m, leq2(m, length1(store)))
if13(store, m, true) -> if23(store, m, empty1(fstsplit2(m, store)))
if13(store, m, false) -> if33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
if23(store, m, false) -> process2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
if33(store, m, false) -> process2(sndsplit2(m, app2(map_f2(self, nil), store)), m)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].


The following pairs can be oriented strictly and are deleted.


FSTSPLIT2(s1(n), cons2(h, t)) -> FSTSPLIT2(n, t)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial Order [17,21] with Interpretation:

POL( cons2(x1, x2) ) = max{0, -1}


POL( s1(x1) ) = x1 + 1


POL( FSTSPLIT2(x1, x2) ) = x1



The following usable rules [14] were oriented: none



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
              ↳ QDP
                ↳ PisEmptyProof
          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
process2(store, m) -> if13(store, m, leq2(m, length1(store)))
if13(store, m, true) -> if23(store, m, empty1(fstsplit2(m, store)))
if13(store, m, false) -> if33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
if23(store, m, false) -> process2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
if33(store, m, false) -> process2(sndsplit2(m, app2(map_f2(self, nil), store)), m)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

PROCESS2(store, m) -> IF13(store, m, leq2(m, length1(store)))
IF13(store, m, false) -> IF33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
IF33(store, m, false) -> PROCESS2(sndsplit2(m, app2(map_f2(self, nil), store)), m)
IF23(store, m, false) -> PROCESS2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
IF13(store, m, true) -> IF23(store, m, empty1(fstsplit2(m, store)))

The TRS R consists of the following rules:

fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
process2(store, m) -> if13(store, m, leq2(m, length1(store)))
if13(store, m, true) -> if23(store, m, empty1(fstsplit2(m, store)))
if13(store, m, false) -> if33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
if23(store, m, false) -> process2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
if33(store, m, false) -> process2(sndsplit2(m, app2(map_f2(self, nil), store)), m)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.